\begin{tabbing}
$\forall$${\it es}$:ES, $i$, $x$, $y$, $z$:Id, ${\it Tx}$, ${\it Ty}$, ${\it Tz}$:Type, $P$:(${\it Tx}$$\rightarrow$${\it Ty}$$\rightarrow$${\it Tz}$$\rightarrow\mathbb{P}$), ${\it Lx}$, ${\it Ly}$, ${\it Lz}$:(Knd List).
\\[0ex]@$i$ only ${\it Lx}$ affect $x$:${\it Tx}$
\\[0ex]$\Rightarrow$ @$i$ only ${\it Ly}$ affect $y$:${\it Ty}$
\\[0ex]$\Rightarrow$ @$i$ only ${\it Lz}$ affect $z$:${\it Tz}$
\\[0ex]$\Rightarrow$ @$i$($x$:${\it Tx}$)
\\[0ex]$\Rightarrow$ @$i$($y$:${\it Ty}$)
\\[0ex]$\Rightarrow$ @$i$($z$:${\it Tz}$)
\\[0ex]$\Rightarrow$ \=$\forall$$e$@$i$.\+
\\[0ex](kind($e$) $\in$ ${\it Lx}$ @ ${\it Ly}$ @ ${\it Lz}$)
\\[0ex]$\Rightarrow$ $P$($x$ when $e$,$y$ when $e$,$z$ when $e$)
\\[0ex]$\Rightarrow$ $P$(($x$ after $e$),($y$ after $e$),($z$ after $e$))
\-\\[0ex]$\Rightarrow$ @$i$ stable ${\it state}$.$P$(${\it state}$.$x$,${\it state}$.$y$,${\it state}$.$z$)  
\end{tabbing}